KILLED



    


Runtime Complexity (full) proof of /tmp/tmpK1Y_FC/Ex4_DLMMU04_C.xml









The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

0 CpxTRS


↳1 DecreasingLoopProof (⇔, 5123 ms)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs


    ↳9 NoRewriteLemmaProof (LOWER BOUND(ID), 39 ms)


    ↳10 typed CpxTrs


    ↳11 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳12 typed CpxTrs


    ↳13 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳14 typed CpxTrs


    ↳15 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳16 typed CpxTrs


    ↳17 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳18 typed CpxTrs


    ↳19 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳20 typed CpxTrs


    ↳21 NoRewriteLemmaProof (LOWER BOUND(ID), 12 ms)


    ↳22 typed CpxTrs


    ↳23 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳24 typed CpxTrs


    ↳25 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳26 typed CpxTrs


    ↳27 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳28 typed CpxTrs


    ↳29 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)


    ↳30 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

active(and(tt, T)) → mark(T)

active(isNatIList(IL)) → mark(isNatList(IL))

active(isNat(0)) → mark(tt)

active(isNat(s(N))) → mark(isNat(N))

active(isNat(length(L))) → mark(isNatList(L))

active(isNatIList(zeros)) → mark(tt)

active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))

active(isNatList(nil)) → mark(tt)

active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))

active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))

active(zeros) → mark(cons(0, zeros))

active(take(0, IL)) → mark(uTake1(isNatIList(IL)))

active(uTake1(tt)) → mark(nil)

active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))

active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))

active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))

active(uLength(tt, L)) → mark(s(length(L)))

active(and(X1, X2)) → and(active(X1), X2)

active(and(X1, X2)) → and(X1, active(X2))

active(s(X)) → s(active(X))

active(length(X)) → length(active(X))

active(cons(X1, X2)) → cons(active(X1), X2)

active(take(X1, X2)) → take(active(X1), X2)

active(take(X1, X2)) → take(X1, active(X2))

active(uTake1(X)) → uTake1(active(X))

active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)

active(uLength(X1, X2)) → uLength(active(X1), X2)

and(mark(X1), X2) → mark(and(X1, X2))

and(X1, mark(X2)) → mark(and(X1, X2))

s(mark(X)) → mark(s(X))

length(mark(X)) → mark(length(X))

cons(mark(X1), X2) → mark(cons(X1, X2))

take(mark(X1), X2) → mark(take(X1, X2))

take(X1, mark(X2)) → mark(take(X1, X2))

uTake1(mark(X)) → mark(uTake1(X))

uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))

uLength(mark(X1), X2) → mark(uLength(X1, X2))

proper(and(X1, X2)) → and(proper(X1), proper(X2))

proper(tt) → ok(tt)

proper(isNatIList(X)) → isNatIList(proper(X))

proper(isNatList(X)) → isNatList(proper(X))

proper(isNat(X)) → isNat(proper(X))

proper(0) → ok(0)

proper(s(X)) → s(proper(X))

proper(length(X)) → length(proper(X))

proper(zeros) → ok(zeros)

proper(cons(X1, X2)) → cons(proper(X1), proper(X2))

proper(nil) → ok(nil)

proper(take(X1, X2)) → take(proper(X1), proper(X2))

proper(uTake1(X)) → uTake1(proper(X))

proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))

proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))

and(ok(X1), ok(X2)) → ok(and(X1, X2))

isNatIList(ok(X)) → ok(isNatIList(X))

isNatList(ok(X)) → ok(isNatList(X))

isNat(ok(X)) → ok(isNat(X))

s(ok(X)) → ok(s(X))

length(ok(X)) → ok(length(X))

cons(ok(X1), ok(X2)) → ok(cons(X1, X2))

take(ok(X1), ok(X2)) → ok(take(X1, X2))

uTake1(ok(X)) → ok(uTake1(X))

uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))

uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))

top(mark(X)) → top(proper(X))

top(ok(X)) → top(active(X))

Rewrite Strategy: FULL




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
and(mark(X1), X2) →+ mark(and(X1, X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [X1 / mark(X1)].
The result substitution is [ ].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

active(and(tt, T)) → mark(T)

active(isNatIList(IL)) → mark(isNatList(IL))

active(isNat(0')) → mark(tt)

active(isNat(s(N))) → mark(isNat(N))

active(isNat(length(L))) → mark(isNatList(L))

active(isNatIList(zeros)) → mark(tt)

active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))

active(isNatList(nil)) → mark(tt)

active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))

active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))

active(zeros) → mark(cons(0', zeros))

active(take(0', IL)) → mark(uTake1(isNatIList(IL)))

active(uTake1(tt)) → mark(nil)

active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))

active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))

active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))

active(uLength(tt, L)) → mark(s(length(L)))

active(and(X1, X2)) → and(active(X1), X2)

active(and(X1, X2)) → and(X1, active(X2))

active(s(X)) → s(active(X))

active(length(X)) → length(active(X))

active(cons(X1, X2)) → cons(active(X1), X2)

active(take(X1, X2)) → take(active(X1), X2)

active(take(X1, X2)) → take(X1, active(X2))

active(uTake1(X)) → uTake1(active(X))

active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)

active(uLength(X1, X2)) → uLength(active(X1), X2)

and(mark(X1), X2) → mark(and(X1, X2))

and(X1, mark(X2)) → mark(and(X1, X2))

s(mark(X)) → mark(s(X))

length(mark(X)) → mark(length(X))

cons(mark(X1), X2) → mark(cons(X1, X2))

take(mark(X1), X2) → mark(take(X1, X2))

take(X1, mark(X2)) → mark(take(X1, X2))

uTake1(mark(X)) → mark(uTake1(X))

uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))

uLength(mark(X1), X2) → mark(uLength(X1, X2))

proper(and(X1, X2)) → and(proper(X1), proper(X2))

proper(tt) → ok(tt)

proper(isNatIList(X)) → isNatIList(proper(X))

proper(isNatList(X)) → isNatList(proper(X))

proper(isNat(X)) → isNat(proper(X))

proper(0') → ok(0')

proper(s(X)) → s(proper(X))

proper(length(X)) → length(proper(X))

proper(zeros) → ok(zeros)

proper(cons(X1, X2)) → cons(proper(X1), proper(X2))

proper(nil) → ok(nil)

proper(take(X1, X2)) → take(proper(X1), proper(X2))

proper(uTake1(X)) → uTake1(proper(X))

proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))

proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))

and(ok(X1), ok(X2)) → ok(and(X1, X2))

isNatIList(ok(X)) → ok(isNatIList(X))

isNatList(ok(X)) → ok(isNatList(X))

isNat(ok(X)) → ok(isNat(X))

s(ok(X)) → ok(s(X))

length(ok(X)) → ok(length(X))

cons(ok(X1), ok(X2)) → ok(cons(X1, X2))

take(ok(X1), ok(X2)) → ok(take(X1, X2))

uTake1(ok(X)) → ok(uTake1(X))

uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))

uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))

top(mark(X)) → top(proper(X))

top(ok(X)) → top(active(X))

S is empty.
Rewrite Strategy: FULL




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
active, isNatList, isNat, and, isNatIList, cons, uTake1, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
isNatList < active
isNat < active
and < active
isNatIList < active
cons < active
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
isNatList < proper
isNat < proper
and < proper
isNatIList < proper
cons < proper
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(8) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
isNatList, active, isNat, and, isNatIList, cons, uTake1, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
isNatList < active
isNat < active
and < active
isNatIList < active
cons < active
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
isNatList < proper
isNat < proper
and < proper
isNatIList < proper
cons < proper
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isNatList.




(10) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
isNat, active, and, isNatIList, cons, uTake1, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
isNat < active
and < active
isNatIList < active
cons < active
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
isNat < proper
and < proper
isNatIList < proper
cons < proper
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isNat.




(12) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
and, active, isNatIList, cons, uTake1, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
and < active
isNatIList < active
cons < active
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
and < proper
isNatIList < proper
cons < proper
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol and.




(14) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
isNatIList, active, cons, uTake1, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
isNatIList < active
cons < active
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
isNatIList < proper
cons < proper
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol isNatIList.




(16) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
cons, active, uTake1, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
cons < active
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
cons < proper
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol cons.




(18) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
uTake1, active, uTake2, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
uTake1 < active
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
uTake1 < proper
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol uTake1.




(20) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
uTake2, active, take, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
uTake2 < active
take < active
uLength < active
s < active
length < active
active < top
uTake2 < proper
take < proper
uLength < proper
s < proper
length < proper
proper < top




(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol uTake2.




(22) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
take, active, uLength, s, length, proper, top
They will be analysed ascendingly in the following order:
take < active
uLength < active
s < active
length < active
active < top
take < proper
uLength < proper
s < proper
length < proper
proper < top




(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol take.




(24) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
uLength, active, s, length, proper, top
They will be analysed ascendingly in the following order:
uLength < active
s < active
length < active
active < top
uLength < proper
s < proper
length < proper
proper < top




(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol uLength.




(26) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
s, active, length, proper, top
They will be analysed ascendingly in the following order:
s < active
length < active
active < top
s < proper
length < proper
proper < top




(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol s.




(28) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
length, active, proper, top
They will be analysed ascendingly in the following order:
length < active
active < top
length < proper
proper < top




(29) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol length.




(30) Obligation:
TRS:
Rules:
active(and(tt, T)) → mark(T)
active(isNatIList(IL)) → mark(isNatList(IL))
active(isNat(0')) → mark(tt)
active(isNat(s(N))) → mark(isNat(N))
active(isNat(length(L))) → mark(isNatList(L))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(N, L))) → mark(and(isNat(N), isNatList(L)))
active(isNatList(take(N, IL))) → mark(and(isNat(N), isNatIList(IL)))
active(zeros) → mark(cons(0', zeros))
active(take(0', IL)) → mark(uTake1(isNatIList(IL)))
active(uTake1(tt)) → mark(nil)
active(take(s(M), cons(N, IL))) → mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL))
active(uTake2(tt, M, N, IL)) → mark(cons(N, take(M, IL)))
active(length(cons(N, L))) → mark(uLength(and(isNat(N), isNatList(L)), L))
active(uLength(tt, L)) → mark(s(length(L)))
active(and(X1, X2)) → and(active(X1), X2)
active(and(X1, X2)) → and(X1, active(X2))
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))
active(uTake1(X)) → uTake1(active(X))
active(uTake2(X1, X2, X3, X4)) → uTake2(active(X1), X2, X3, X4)
active(uLength(X1, X2)) → uLength(active(X1), X2)
and(mark(X1), X2) → mark(and(X1, X2))
and(X1, mark(X2)) → mark(and(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))
uTake1(mark(X)) → mark(uTake1(X))
uTake2(mark(X1), X2, X3, X4) → mark(uTake2(X1, X2, X3, X4))
uLength(mark(X1), X2) → mark(uLength(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(isNatIList(X)) → isNatIList(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNat(X)) → isNat(proper(X))
proper(0') → ok(0')
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(nil) → ok(nil)
proper(take(X1, X2)) → take(proper(X1), proper(X2))
proper(uTake1(X)) → uTake1(proper(X))
proper(uTake2(X1, X2, X3, X4)) → uTake2(proper(X1), proper(X2), proper(X3), proper(X4))
proper(uLength(X1, X2)) → uLength(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNatIList(ok(X)) → ok(isNatIList(X))
isNatList(ok(X)) → ok(isNatList(X))
isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
take(ok(X1), ok(X2)) → ok(take(X1, X2))
uTake1(ok(X)) → ok(uTake1(X))
uTake2(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(uTake2(X1, X2, X3, X4))
uLength(ok(X1), ok(X2)) → ok(uLength(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Types:
active :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
and :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
tt :: tt:mark:0':zeros:nil:ok
mark :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatIList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNatList :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
isNat :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
0' :: tt:mark:0':zeros:nil:ok
s :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
length :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
zeros :: tt:mark:0':zeros:nil:ok
cons :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
nil :: tt:mark:0':zeros:nil:ok
take :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake1 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uTake2 :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
uLength :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
proper :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
ok :: tt:mark:0':zeros:nil:ok → tt:mark:0':zeros:nil:ok
top :: tt:mark:0':zeros:nil:ok → top
hole_tt:mark:0':zeros:nil:ok1_0 :: tt:mark:0':zeros:nil:ok
hole_top2_0 :: top
gen_tt:mark:0':zeros:nil:ok3_0 :: Nat → tt:mark:0':zeros:nil:ok
Generator Equations:
gen_tt:mark:0':zeros:nil:ok3_0(0) ⇔ tt
gen_tt:mark:0':zeros:nil:ok3_0(+(x, 1)) ⇔ mark(gen_tt:mark:0':zeros:nil:ok3_0(x))
The following defined symbols remain to be analysed:
active, proper, top
They will be analysed ascendingly in the following order:
active < top
proper < top